/*
 * The ELepHant Reasoner
 *
 * Copyright (C) Baris Sertkaya (sertkaya.baris@gmail.com)
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */


#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <assert.h>
#include <pthread.h>
#include <sys/types.h>

#include "../model/datatypes.h"
#include "../model/model.h"
#include "../model/utils.h"
#include "../model/limits.h"
#include "../utils/stack.h"
#include "../index/utils.h"
#include "../hashing/key_hash_table.h"
#include "../hashing/key_value_hash_table.h"
#include "utils.h"
#include "saturation_worker.h"

// for statistics
int saturation_unique_subsumption_count = 0, saturation_total_subsumption_count = 0;
int saturation_unique_link_count = 0, saturation_total_link_count = 0;

int number_of_threads = 4;

// mutex for synchronizing access to the scheduled concepts
pthread_mutex_t scheduled_concepts_mutex;

/*
 * Saturates the concepts of a given TBox.
 * Returns:
 * 	-1: If the KB is inconsistent. In this case it immediately returns, i.e., saturation process
 * 	is cancelled.
 * 	0: Otherwise
 */
char saturate_concepts(KB* kb) {
	TBox* tbox = kb->tbox;

	// array for the threads
	pthread_t threads[number_of_threads];

	// the worker data, same for all workers
	struct saturation_worker_data worker_data;
	init_stack(&(worker_data.scheduled_concepts));

	// push the initial axioms to the scheduled_axioms stack of each atomic concept,
	// and push the atomic concepts to the stack of scheduled_concepts in the worker data.
	int i, j;

	for (i = 0; i < tbox->atomic_concept_count ; ++i) {
		for (j = 0; j < tbox->atomic_concept_list[i]->told_subsumer_count; ++j)
			push(&(tbox->atomic_concept_list[i]->scheduled_axioms), create_concept_saturation_axiom(tbox->atomic_concept_list[i], tbox->atomic_concept_list[i]->told_subsumers[j], NULL, SUBSUMPTION_INITIALIZATION));
		push(&(worker_data.scheduled_concepts), tbox->atomic_concept_list[i]);
		tbox->atomic_concept_list[i]->is_scheduled = 1;
	}

	// The hash of nominals that are generated during preprocessing.
	Node* node = last_node(kb->generated_nominals);
	Concept* nominal = NULL;
	// The input axioms generated from concept and role assertions
	while (node) {
		nominal = (Concept*) node->value;
		for (j = 0; j < nominal->told_subsumer_count; ++j)
			push(&(nominal->scheduled_axioms), create_concept_saturation_axiom(nominal, nominal->told_subsumers[j], NULL, SUBSUMPTION_INITIALIZATION));
		push(&(worker_data.scheduled_concepts), nominal);
		nominal->is_scheduled = 1;
		node = previous_node(node);
	}


	// initialize the mutex for scheduled_concepts
	if (pthread_mutex_init(&(scheduled_concepts_mutex), NULL) != 0) {
		fprintf(stderr, "saturate_concepts: Mutex initialization failed, aborting\n");
		exit(EXIT_FAILURE);
	}

	int thread_creation_result;
	for (i = 0; i < number_of_threads; ++i)
		if ((thread_creation_result = pthread_create(&threads[i], NULL, saturation_worker, (void*) &worker_data))) {
			fprintf(stderr, "Thread creation failed: %d\n", thread_creation_result);
			exit(EXIT_FAILURE);
		}

	for (i = 0; i < number_of_threads; ++i)
		pthread_join(threads[i], NULL);

	// printf("Total subsumptions:%d\nUnique subsumptions:%d\n", saturation_total_subsumption_count, saturation_unique_subsumption_count);
	// printf("Total links:%d\nUnique links:%d\n", saturation_total_link_count, saturation_unique_link_count);

	return 0;
}
